\label{check_function}

\paragraph{}

\texttt{Verification functions} are functions which can be called 
within the \texttt{verification expression}. Their is two kinds of 
verification functions :
\begin {itemize}
\item \texttt{set-based functions}, which always takes a set or
element as first parameter, and can have others parameters 
(usually literal). They always returns a value or a list of values. 
eg : Cardinal, Get\_Property\_Value, Property\_Exists;
\item \texttt{value manipulation functions}, where the single 
parameter is a value or a list of values, and which returns another 
value.
\end {itemize}

\subsubsection {Property\_Exists}

\textit {Property\_Exists} takes two parameters, an element
or a set and a string literal. If the first argument is an 
element, then it returns true if the specified property is 
defined on this element, and else in the other case.
If the first argument is a set, it returns true if all the
the specified property is defined on all the elements of the 
set. The \textit{Exists} function is an alias of \textit 
{Property\_Exists}.
 
\subsubsection {Get\_Property\_Value}

\textit {Get\_Property\_Value} takes two parameters, an element
or a set and a string literal. It returns the either the value 
of the property whose name is the second parameter in the node 
designed by the first parameter, if the first parameter is an
element, or a a list of values which are the results of the 
application of \textit {Get\_Property\_Value} on each element
of the set. The \textit {Property} function is an alias of the
\textit {Get\_Property\_Value} function.

This is currently the only way to produce a list of values.

\subsubsection {Cardinal}

\textit {Cardinal} takes a set as parameter. It returns the 
set cardinal (ie. an integer).

\subsubsection {First}

\textit{First} is a function which cann be applied on a range or on a 
list of range. It returns respectively a float element (even if the 
actual value of the AADL range term was an integer) or a list of
floats, which are the lower bounds of each range of the list.

Whenever called on a empty list, it returns another empty list. 
However, when called on a nil argument, it returns an error and
the theorem is therefore considered false.

\subsubsection {Last}

\textit{Last} is a function which can be applied on a range or on a 
list of range. It returns respectively a float element (even if the 
actual value of the AADL range term was an integer) or a list of
floats, which are the Upper bounds of each range of the list.

Whenever called on a empty list, it returns another empty list. 
However, when called on a nil argument, it returns an error and
the theorem is therefore considered false.

\subsubsection {List}

\textit{List} is a function which can be applied on a set of 
literals, or on a REAL \textit{Set}. In the first case, it
build a list that contains the values given as paremeters. In 
the second case, it build a list of \textit{Elements} which are 
the set's elements.

\subsubsection {Size}

\textit{Size} is a function which can be applied on any kind of list. 
It returns the number of elements in the list (an integer value).

\subsubsection {Head}

\textit{Head} is a function which can be applied on any kind of list. 
It returns the first element of the list (ie. on a list of integers, 
it will return an interger).

Whenever called on a empty list, it returns an error and the theorem 
is therefore considered false. Thus, test should be done using a 
ternary expression and the \textit{Size} function on the list.

\subsubsection {Queue}

\textit{Queue} is a function which can be applied on any kind of list. 
It returns the list without the first element.

Whenever called on a empty list, it returns an error and the theorem 
is therefore considered false. Thus, test should be done using a 
ternary expression and the \textit{Size} function on the list.

 \subsubsection {Max}

\textit {Max} is a function which can be applied on a list of 
floats or integers as parameter. It always return a float which 
is the highest value found. Note that the only way to produce 
the list is currently to call the Get\_Property\_Value on a list.
 
\subsubsection {Min}

\textit {Min} is a function which can be applied on a list of 
floats or integers as parameter. It always return a float which 
is the lowest value found. Note that the only way to produce the 
list is currently to call the Get\_Property\_Value on a list.
 
\subsubsection {Sum}

\textit {Sum} is a function which can be applied on a list of 
floats or integers as parameter. It always return a float which 
is the sum of all the values found. Note that the only way to 
produce the list is currently to call the Get\_Property\_Value 
on a list.

\subsubsection {Product}

\textit {Product} is a function which can be applied on a list 
of floats or integers as parameter. It always return a float 
which is the product of all the values found. Note that the 
only way to produce the list is currently to call the 
Get\_Property\_Value on a list.

\subsubsection {GCD}

\textit {GCD} is a function which can be applied on a list of 
floats or integers as parameter. It always return a float 
which is the Greatest Common Divisor of all the values 
found. Note that the only way to produce the list is 
currently to call the Get\_Property\_Value on a list.

\subsubsection {LCM}

\textit {LCM} is a function which can be applied on a list of 
floats or integers as parameter. It always return a float 
which is the Lowest Common Multiple of all the values 
found. Note that the only way to produce the list is 
currently to call the Get\_Property\_Value on a list.
